T:Type, n:, f:(int_seg(0; n)T), i:int_seg(0; n). mklist(n; f)[i] = f(i) 

latex

Definitions	False, A, A  B, ge(i; j), P  Q, t  T, x:A. B(x), P  Q, lelt(i; j; k), suptype(S; T), subtype(S; T), int_seg(i; j), ff, tt, if b then t else f fi , Y, primrec(n; b; c), mklist(n; f), prop{i:l}, , P  Q, P  Q, guard(T), sq_type(T), t  ...$L, ||as||, i <z j, b, i z j, nth_tl(n;as), hd(l), l[i], Unit, , P  Q, decidable(P),
Lemmas	ge wf, nat properties, nat wf, int seg wf, le wf, not functionality wrt iff, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, iff transitivity, not wf, bnot wf, assert wf, bool wf, eq int wf, decidable lt, length wf1, mklist wf, select append front, mklist length, select append back, non neg length, length cons, length nil